COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00005 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.bb Note on comprehension

	The ideal set theory would be Cantor's with an unrestricted
comprehension axiom schema.  With such a schema, the axioms of
⊗pairing, ⊗unions, and %2power set%1 could be dispensed with, although the
axioms of ⊗extensionality, ⊗infinity, ⊗regularity and ⊗choice would still
be required.  Unfortunately, Cantor set theory is inconsistent, but
we would like to re-establish as much of it as possible.  Here are
some ideas:

	We begin with questions about unrestricted comprehension
terms α{x|P(x)α}.

.item←0
	#. Which terms can be shown to exist in ZF, i.e. for which
formulas ⊗P(x) can we prove the existence of a set ⊗a satisfying

!!a1:	%2∀x.(x_ε_a_≡_P(x))%1?

	#. For which ⊗P(x) is ({eq a1}) consistent with any consistent
extension of ZF?  I guess this must be the same as the answer to the
previous question.

	#. Which sets of ⊗P(x) are consistent with ZF?

	#. Which sets of ⊗P(x) are consistent with just extensionality?

	#. Is there a nice way of extending the comprehension axiom
that obviates the need for ⊗pairing, ⊗unions and %2power set%1?

	#. Is there any nice maximal set of comprehension terms, such
that adding more will produce inconsistency?  My guess is that there
are such maximal sets, and they can be profitably studied, but
such a maximal set is not recursively enumerable.

This is SET.NOT[W78,JMC] and was pubbed on {date} at {time}.